So what we have is we have a little calculus that actually helps our agent in

dealing with world models that can be expressed in propositional logic. And

we'll see that the Mumpus world is one such, Mary and Bill and John is one such

and many many other examples as well. So we have inference kind of under control.

We're going to see that inference is actually terminating, is the decision

procedure. We're going to see that there's even better inference procedures.

So for a couple of tens and a couple of hundreds even to a couple of thousands

of variables, tableaus work well. If you go into the hundred thousands to a

million variable kind of formulae, then you want something better and that's

what we're going to look at next. So we were talking about tableaus. Tableaus as

inference procedures that can tell me about entailment. Entailment, remember,

means that in all situations that make the antecedents true, also the

succidents are true, which is exactly what the agent needs. It knows certain

things that it has sensed and in an ideal world where sensing is reliable,

the things you can see are actually true. We're going to relax that in the

next semester. So we have things that kind of look like axioms or hypotheses

here and entailment gives us additional information, which is exactly what the

what the agent needs. So we have a basic procedure and that works well, except of

course it doesn't. For instance, we had to do unspeakable things when we were

having disjunctions and implications. Okay, what can we do? Well, time for

engineering. You can remember, oh there are these propositional identities. We

always know that phi and phi is phi, right, or phi and phi or psi is phi or

something like this. You could actually kind of try and simplify with these,

which you sometimes do. This is not good, right. You have your wonderful

little program and you stuff all the things and the kitchen sink in there and

have all these kind of everything, oh I know this, I know that, and well let's

make lots of junk code in my, right. We shouldn't need that, okay. We could do

this but that's not the right way. What we can do is something else. We can make

the calculus better by adding additional rules. Here's an example. If I have an A

true and an A implies B true, then I can in the abstract do what I've done, right,

which is a not A or B true, which is a not not not A or not B true, and then I

can tableau away and one thing I notice is that I end up with a tableau which

kind of has the old stuff in it and makes one new thing, namely B true, which

is something I can actually make into a macro step because this kind of

abstract computation, abstract derivation tells me whenever I see an A true and an

A implies B true, then I can just add a B true. It's kind of a mega step or

shortcut. So I can make this rule and add it to my tableau calculus. Does that sound?

Well if you believe the old calculus is sound, then this is sound because I can

replace this by a big proof in the smaller calculus. We call rules like that

derivable because they stand for a macro derivation. The nice thing is I can do

that in a variety of other cases. Here's I've written down a couple more. They all

expand to a bigger proof which means I can add them to my tableau calculus

without changing the calculus because I could always kind of expand it into a

terribly long and big calculus in the original calculus. Or in other words if

the old five rule calculus was sound, then the six, seven, eight, nine, ten, eleven,

twelve rule calculus which I have on the board here is sound as well. How about

completeness?

Yeah it still remains complete because we don't lose the possibility to prove

things that we could before because we maintain the five original rules. So we

are still able to prove all theories that we could before. Excellent! You don't